\begin{tabbing}
$\forall$\=${\it es}$:ES, ${\it Config}$:AbsInterface(chain\_config()), ${\it Cmd}$:Type, ${\it Sys}$:AbsInterface(chain\_sys(${\it Cmd}$)),\+
\\[0ex]$e$:E.
\-\\[0ex](0 $<$ $\parallel$cmd{-}history($e$)$\parallel$) $\Rightarrow$ ($\exists$${\it e'}$:E. (${\it e'}$ $\leq$loc $e$  \& ($\uparrow$(${\it e'}$ $\in_{b}$ ${\it Sys}$(valid)))))
\end{tabbing}